KILLED
Runtime Complexity (innermost) proof of /tmp/tmpJgoWXl/int.xml
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).
0 CpxRelTRS
↳1 DecreasingLoopProof (⇔, 13.0 s)
↳2 BOUNDS(n^1, INF)
↳3 RenamingProof (⇔, 0 ms)
↳4 CpxRelTRS
↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 typed CpxTrs
↳7 OrderProof (LOWER BOUND(ID), 0 ms)
↳8 typed CpxTrs
↳9 NoRewriteLemmaProof (LOWER BOUND(ID), 52 ms)
↳10 typed CpxTrs
↳11 NoRewriteLemmaProof (LOWER BOUND(ID), 0 ms)
↳12 typed CpxTrs
(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
eeval(Fun(n, e), ns, vs, p) → eeval[False][Let](Fun(n, e), ns, vs, p, lookbody(n, p))
eeval(Eq(f, s), ns, vs, p) → eeval[True][Ite](eqExp(eeval(f, ns, vs, p), eeval(s, ns, vs, p)), Eq(f, s), ns, vs, p)
eeval(Error(e11, e12), ns, vs, p) → eeval[False][Ite](False, Error(e11, e12), ns, vs, p)
eeval(F, ns, vs, p) → F
eeval(T, ns, vs, p) → T
eeval(ITE(i, t, e), ns, vs, p) → eeval[Ite](checkConstrExp(eeval(i, ns, vs, p), T), ITE(i, t, e), ns, vs, p)
eeval(Bsf(op, t1, t2), ns, vs, p) → eeval[Let](Bsf(op, t1, t2), ns, vs, p, eeval(t1, ns, vs, p))
eeval(Var(int), ns, vs, p) → lookvar(int, ns, vs)
run(Cons(Fun(f0, e), xs), input) → run[Let][Let](Cons(Fun(f0, e), xs), input, f0, lookbody(f0, Cons(Fun(f0, e), xs)))
eqExp(Error(e11, e12), Error(e21, e22)) → and(eqExp(e11, e21), eqExp(e12, e22))
eqExp(Error(e11, e12), F) → False
eqExp(Error(e11, e12), T) → False
eqExp(Error(e11, e12), Fun(fn2, fe2)) → False
eqExp(Error(e11, e12), Eq(eq21, eq22)) → False
eqExp(Error(e11, e12), ITE(i2, t2, e2)) → False
eqExp(Error(e11, e12), Bsf(op2, b21, b22)) → False
eqExp(Error(e11, e12), Var(v2)) → False
eqExp(F, Error(e21, e22)) → False
eqExp(F, F) → True
eqExp(F, T) → False
eqExp(F, Fun(fn2, fe2)) → False
eqExp(F, Eq(eq21, eq22)) → False
eqExp(F, ITE(i2, t2, e2)) → False
eqExp(F, Bsf(op2, b21, b22)) → False
eqExp(F, Var(v2)) → False
eqExp(T, Error(e21, e22)) → False
eqExp(T, F) → False
eqExp(T, T) → True
eqExp(T, Fun(fn2, fe2)) → False
eqExp(T, Eq(eq21, eq22)) → False
eqExp(T, ITE(i2, t2, e2)) → False
eqExp(T, Bsf(op2, b21, b22)) → False
eqExp(T, Var(v2)) → False
eqExp(Fun(fn1, fe1), Error(e21, e22)) → False
eqExp(Fun(fn1, fe1), F) → False
eqExp(Fun(fn1, fe1), T) → False
eqExp(Fun(fn1, fe1), Fun(fn2, fe2)) → and(!EQ(fn1, fn2), eqExp(fe1, fe2))
eqExp(Fun(fn1, fe1), Eq(eq21, eq22)) → False
eqExp(Fun(fn1, fe1), ITE(i2, t2, e2)) → False
eqExp(Fun(fn1, fe1), Bsf(op2, b21, b22)) → False
eqExp(Fun(fn1, fe1), Var(v2)) → False
eqExp(Eq(eq11, eq12), Error(e21, e22)) → False
eqExp(Eq(eq11, eq12), F) → False
eqExp(Eq(eq11, eq12), T) → False
eqExp(Eq(eq11, eq12), Fun(fn2, fe2)) → False
eqExp(Eq(eq11, eq12), Eq(eq21, eq22)) → and(eqExp(eq11, eq21), eqExp(eq12, eq22))
eqExp(Eq(eq11, eq12), ITE(i2, t2, e2)) → False
eqExp(Eq(eq11, eq12), Bsf(op2, b21, b22)) → False
eqExp(Eq(eq11, eq12), Var(v2)) → False
eqExp(ITE(i1, t1, e1), Error(e21, e22)) → False
eqExp(ITE(i1, t1, e1), F) → False
eqExp(ITE(i1, t1, e1), T) → False
eqExp(ITE(i1, t1, e1), Fun(fn2, fe2)) → False
eqExp(ITE(i1, t1, e1), Eq(eq21, eq22)) → False
eqExp(ITE(i1, t1, e1), ITE(i2, t2, e2)) → and(eqExp(i1, i2), and(eqExp(t1, t2), eqExp(e1, e2)))
eqExp(ITE(i1, t1, e1), Bsf(op2, b21, b22)) → False
eqExp(ITE(i1, t1, e1), Var(v2)) → False
eqExp(Bsf(op1, b11, b12), Error(e21, e22)) → False
eqExp(Bsf(op1, b11, b12), F) → False
eqExp(Bsf(op1, b11, b12), T) → False
eqExp(Bsf(op1, b11, b12), Fun(fn2, fe2)) → False
eqExp(Bsf(op1, b11, b12), Eq(eq21, eq22)) → False
eqExp(Bsf(op1, b11, b12), ITE(i2, t2, e2)) → False
eqExp(Bsf(o1, b11, b12), Bsf(o2, b21, b22)) → and(True, and(eqExp(b11, b21), eqExp(b12, b22)))
eqExp(Bsf(op1, b11, b12), Var(v2)) → False
eqExp(Var(v1), Error(e21, e22)) → False
eqExp(Var(v1), F) → False
eqExp(Var(v1), T) → False
eqExp(Var(v1), Fun(fn2, fe2)) → False
eqExp(Var(v1), Eq(eq21, eq22)) → False
eqExp(Var(v1), ITE(i2, t2, e2)) → False
eqExp(Var(v1), Bsf(op2, b21, b22)) → False
eqExp(Var(v1), Var(v2)) → !EQ(v1, v2)
checkConstrExp(Error(e11, e12), Error(e21, e22)) → True
checkConstrExp(Error(e11, e12), F) → False
checkConstrExp(Error(e11, e12), T) → False
checkConstrExp(Error(e11, e12), Fun(fn2, fe2)) → False
checkConstrExp(Error(e11, e12), Eq(eq21, eq22)) → False
checkConstrExp(Error(e11, e12), ITE(i2, t2, e2)) → False
checkConstrExp(Error(e11, e12), Bsf(op2, b21, b22)) → False
checkConstrExp(Error(e11, e12), Var(v2)) → False
checkConstrExp(F, Error(e21, e22)) → False
checkConstrExp(F, F) → True
checkConstrExp(F, T) → False
checkConstrExp(F, Fun(fn2, fe2)) → False
checkConstrExp(F, Eq(eq21, eq22)) → False
checkConstrExp(F, ITE(i2, t2, e2)) → False
checkConstrExp(F, Bsf(op2, b21, b22)) → False
checkConstrExp(F, Var(v2)) → False
checkConstrExp(T, Error(e21, e22)) → False
checkConstrExp(T, F) → False
checkConstrExp(T, T) → True
checkConstrExp(T, Fun(fn2, fe2)) → False
checkConstrExp(T, Eq(eq21, eq22)) → False
checkConstrExp(T, ITE(i2, t2, e2)) → False
checkConstrExp(T, Bsf(op2, b21, b22)) → False
checkConstrExp(T, Var(v2)) → False
checkConstrExp(Fun(fn1, fe1), Error(e21, e22)) → False
checkConstrExp(Fun(fn1, fe1), F) → False
checkConstrExp(Fun(fn1, fe1), T) → False
checkConstrExp(Fun(fn1, fe1), Fun(fn2, fe2)) → True
checkConstrExp(Fun(fn1, fe1), Eq(eq21, eq22)) → False
checkConstrExp(Fun(fn1, fe1), ITE(i2, t2, e2)) → False
checkConstrExp(Fun(fn1, fe1), Bsf(op2, b21, b22)) → False
checkConstrExp(Fun(fn1, fe1), Var(v2)) → False
checkConstrExp(Eq(eq11, eq12), Error(e21, e22)) → False
checkConstrExp(Eq(eq11, eq12), F) → False
checkConstrExp(Eq(eq11, eq12), T) → False
checkConstrExp(Eq(eq11, eq12), Fun(fn2, fe2)) → False
checkConstrExp(Eq(eq11, eq12), Eq(eq21, eq22)) → True
checkConstrExp(Eq(eq11, eq12), ITE(i2, t2, e2)) → False
checkConstrExp(Eq(eq11, eq12), Bsf(op2, b21, b22)) → False
checkConstrExp(Eq(eq11, eq12), Var(v2)) → False
checkConstrExp(ITE(i1, t1, e1), Error(e21, e22)) → False
checkConstrExp(ITE(i1, t1, e1), F) → False
checkConstrExp(ITE(i1, t1, e1), T) → False
checkConstrExp(ITE(i1, t1, e1), Fun(fn2, fe2)) → False
checkConstrExp(ITE(i1, t1, e1), Eq(eq21, eq22)) → False
checkConstrExp(ITE(i1, t1, e1), ITE(i2, t2, e2)) → True
checkConstrExp(ITE(i1, t1, e1), Bsf(op2, b21, b22)) → False
checkConstrExp(ITE(i1, t1, e1), Var(v2)) → False
checkConstrExp(Bsf(op1, b11, b12), Error(e21, e22)) → False
checkConstrExp(Bsf(op1, b11, b12), F) → False
checkConstrExp(Bsf(op1, b11, b12), T) → False
checkConstrExp(Bsf(op1, b11, b12), Fun(fn2, fe2)) → False
checkConstrExp(Bsf(op1, b11, b12), Eq(eq21, eq22)) → False
checkConstrExp(Bsf(op1, b11, b12), ITE(i2, t2, e2)) → False
checkConstrExp(Bsf(op1, b11, b12), Bsf(op2, b21, b22)) → True
checkConstrExp(Bsf(op1, b11, b12), Var(v2)) → False
checkConstrExp(Var(v1), Error(e21, e22)) → False
checkConstrExp(Var(v1), F) → False
checkConstrExp(Var(v1), T) → False
checkConstrExp(Var(v1), Fun(fn2, fe2)) → False
checkConstrExp(Var(v1), Eq(eq21, eq22)) → False
checkConstrExp(Var(v1), ITE(i2, t2, e2)) → False
checkConstrExp(Var(v1), Bsf(op2, b21, b22)) → False
checkConstrExp(Var(v1), Var(v2)) → True
lookname(f, Cons(Fun(n, e), xs)) → lookname[Ite](!EQ(f, n), f, Cons(Fun(n, e), xs))
lookbody(f, Cons(Fun(n, e), xs)) → lookbody[Ite](!EQ(f, n), f, Cons(Fun(n, e), xs))
getVar(Var(int)) → int
getIfTrue(ITE(i, t, e)) → t
getIfGuard(ITE(i, t, e)) → i
getIfFalse(ITE(i, t, e)) → e
getFuncName(Fun(n, e)) → n
getFuncExp(Fun(n, e)) → e
getEqSecond(Eq(f, s)) → s
getEqFirst(Eq(f, s)) → f
getConst(Cst(int)) → int
getBsfSecondTerm(Bsf(op, t1, t2)) → t2
getBsfOp(Bsf(op, t1, t2)) → op
getBsfFirstTerm(Bsf(op, t1, t2)) → t1
apply(op, v1, v2) → apply[Ite](eqExp(v1, v2), op, v1, v2)
lookvar(x', Cons(x, xs), vs) → lookvar[Ite](!EQ(x', x), x', Cons(x, xs), vs)
eqOps(o1, o2) → True
The (relative) TRS S consists of the following rules:
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
eeval[False][Ite](True, Eq(f, s), ns, vs, p) → eeval[True][Ite](eqExp(eeval(f, ns, vs, p), eeval(s, ns, vs, p)), Eq(f, s), ns, vs, p)
lookvar[Ite](False, x', Cons(x'', xs'), Cons(x, xs)) → lookvar(x', xs', xs)
lookname[Ite](True, f, Cons(Fun(n, e), xs)) → n
lookbody[Ite](True, f, Cons(Fun(n, e), xs)) → e
eeval[False][Ite](False, Fun(n, e), ns, vs, p) → eeval[False][Let](Fun(n, e), ns, vs, p, lookbody(n, p))
eeval[Ite](False, ITE(i, t, e), ns, vs, p) → eeval(e, ns, vs, p)
eeval[Ite](True, ITE(i, t, e), ns, vs, p) → eeval(t, ns, vs, p)
eeval[False][Let](Fun(n, e), ns, vs, p, ef) → eeval[False][Let][Let](Fun(n, e), ns, vs, p, ef, lookname(n, p))
eeval[False][Let][Let](Fun(n, e), ns, vs, p, ef, nf) → eeval[Let][Let][Let](Fun(n, e), ns, vs, p, ef, nf, eeval(e, ns, vs, p))
eeval[Let](Bsf(op, t1, t2), ns, vs, p, v1) → eeval[Let][Let](Bsf(op, t1, t2), ns, vs, p, v1, eeval(t2, ns, vs, p))
eeval[Let][Let](Bsf(op, t1, t2), ns, vs, p, v1, v2) → apply(op, v1, v2)
lookvar[Ite](True, x', ns, Cons(x, xs)) → x
lookname[Ite](False, f, Cons(x, xs)) → lookname(f, xs)
lookbody[Ite](False, f, Cons(x, xs)) → lookbody(f, xs)
eeval[True][Ite](False, e, ns, vs, p) → F
eeval[True][Ite](True, e, ns, vs, p) → T
apply[Ite](False, op, v1, v2) → F
apply[Ite](True, op, v1, v2) → T
run[Let][Let](p, input, f0, ef) → run[Let](p, input, f0, ef, lookname(f0, p))
run[Let](p, input, f0, ef, nf) → eeval(ef, Cons(nf, Nil), Cons(input, Nil), p)
eeval[Let][Let][Let](e, ns, vs, p, ef, nf, v) → eeval(ef, Cons(nf, Nil), Cons(v, Nil), p)
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
eeval(Fun(0, e), ns, vs, Cons(Fun(0, e1073_3), xs1074_3)) →+ eeval[Let][Let][Let](Fun(0, e), ns, vs, Cons(Fun(0, e1073_3), xs1074_3), e1073_3, 0, eeval(e, ns, vs, Cons(Fun(0, e1073_3), xs1074_3)))
gives rise to a decreasing loop by considering the right hand sides subterm at position [6].
The pumping substitution is [e / Fun(0, e)].
The result substitution is [ ].
(2) BOUNDS(n^1, INF)
(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.
(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
eeval(Fun(n, e), ns, vs, p) → eeval[False][Let](Fun(n, e), ns, vs, p, lookbody(n, p))
eeval(Eq(f, s), ns, vs, p) → eeval[True][Ite](eqExp(eeval(f, ns, vs, p), eeval(s, ns, vs, p)), Eq(f, s), ns, vs, p)
eeval(Error(e11, e12), ns, vs, p) → eeval[False][Ite](False, Error(e11, e12), ns, vs, p)
eeval(F, ns, vs, p) → F
eeval(T, ns, vs, p) → T
eeval(ITE'(i, t, e), ns, vs, p) → eeval[Ite](checkConstrExp(eeval(i, ns, vs, p), T), ITE'(i, t, e), ns, vs, p)
eeval(Bsf(op, t1, t2), ns, vs, p) → eeval[Let](Bsf(op, t1, t2), ns, vs, p, eeval(t1, ns, vs, p))
eeval(Var(int), ns, vs, p) → lookvar(int, ns, vs)
run(Cons(Fun(f0, e), xs), input) → run[Let][Let](Cons(Fun(f0, e), xs), input, f0, lookbody(f0, Cons(Fun(f0, e), xs)))
eqExp(Error(e11, e12), Error(e21, e22)) → and(eqExp(e11, e21), eqExp(e12, e22))
eqExp(Error(e11, e12), F) → False
eqExp(Error(e11, e12), T) → False
eqExp(Error(e11, e12), Fun(fn2, fe2)) → False
eqExp(Error(e11, e12), Eq(eq21, eq22)) → False
eqExp(Error(e11, e12), ITE'(i2, t2, e2)) → False
eqExp(Error(e11, e12), Bsf(op2, b21, b22)) → False
eqExp(Error(e11, e12), Var(v2)) → False
eqExp(F, Error(e21, e22)) → False
eqExp(F, F) → True
eqExp(F, T) → False
eqExp(F, Fun(fn2, fe2)) → False
eqExp(F, Eq(eq21, eq22)) → False
eqExp(F, ITE'(i2, t2, e2)) → False
eqExp(F, Bsf(op2, b21, b22)) → False
eqExp(F, Var(v2)) → False
eqExp(T, Error(e21, e22)) → False
eqExp(T, F) → False
eqExp(T, T) → True
eqExp(T, Fun(fn2, fe2)) → False
eqExp(T, Eq(eq21, eq22)) → False
eqExp(T, ITE'(i2, t2, e2)) → False
eqExp(T, Bsf(op2, b21, b22)) → False
eqExp(T, Var(v2)) → False
eqExp(Fun(fn1, fe1), Error(e21, e22)) → False
eqExp(Fun(fn1, fe1), F) → False
eqExp(Fun(fn1, fe1), T) → False
eqExp(Fun(fn1, fe1), Fun(fn2, fe2)) → and(!EQ(fn1, fn2), eqExp(fe1, fe2))
eqExp(Fun(fn1, fe1), Eq(eq21, eq22)) → False
eqExp(Fun(fn1, fe1), ITE'(i2, t2, e2)) → False
eqExp(Fun(fn1, fe1), Bsf(op2, b21, b22)) → False
eqExp(Fun(fn1, fe1), Var(v2)) → False
eqExp(Eq(eq11, eq12), Error(e21, e22)) → False
eqExp(Eq(eq11, eq12), F) → False
eqExp(Eq(eq11, eq12), T) → False
eqExp(Eq(eq11, eq12), Fun(fn2, fe2)) → False
eqExp(Eq(eq11, eq12), Eq(eq21, eq22)) → and(eqExp(eq11, eq21), eqExp(eq12, eq22))
eqExp(Eq(eq11, eq12), ITE'(i2, t2, e2)) → False
eqExp(Eq(eq11, eq12), Bsf(op2, b21, b22)) → False
eqExp(Eq(eq11, eq12), Var(v2)) → False
eqExp(ITE'(i1, t1, e1), Error(e21, e22)) → False
eqExp(ITE'(i1, t1, e1), F) → False
eqExp(ITE'(i1, t1, e1), T) → False
eqExp(ITE'(i1, t1, e1), Fun(fn2, fe2)) → False
eqExp(ITE'(i1, t1, e1), Eq(eq21, eq22)) → False
eqExp(ITE'(i1, t1, e1), ITE'(i2, t2, e2)) → and(eqExp(i1, i2), and(eqExp(t1, t2), eqExp(e1, e2)))
eqExp(ITE'(i1, t1, e1), Bsf(op2, b21, b22)) → False
eqExp(ITE'(i1, t1, e1), Var(v2)) → False
eqExp(Bsf(op1, b11, b12), Error(e21, e22)) → False
eqExp(Bsf(op1, b11, b12), F) → False
eqExp(Bsf(op1, b11, b12), T) → False
eqExp(Bsf(op1, b11, b12), Fun(fn2, fe2)) → False
eqExp(Bsf(op1, b11, b12), Eq(eq21, eq22)) → False
eqExp(Bsf(op1, b11, b12), ITE'(i2, t2, e2)) → False
eqExp(Bsf(o1, b11, b12), Bsf(o2, b21, b22)) → and(True, and(eqExp(b11, b21), eqExp(b12, b22)))
eqExp(Bsf(op1, b11, b12), Var(v2)) → False
eqExp(Var(v1), Error(e21, e22)) → False
eqExp(Var(v1), F) → False
eqExp(Var(v1), T) → False
eqExp(Var(v1), Fun(fn2, fe2)) → False
eqExp(Var(v1), Eq(eq21, eq22)) → False
eqExp(Var(v1), ITE'(i2, t2, e2)) → False
eqExp(Var(v1), Bsf(op2, b21, b22)) → False
eqExp(Var(v1), Var(v2)) → !EQ(v1, v2)
checkConstrExp(Error(e11, e12), Error(e21, e22)) → True
checkConstrExp(Error(e11, e12), F) → False
checkConstrExp(Error(e11, e12), T) → False
checkConstrExp(Error(e11, e12), Fun(fn2, fe2)) → False
checkConstrExp(Error(e11, e12), Eq(eq21, eq22)) → False
checkConstrExp(Error(e11, e12), ITE'(i2, t2, e2)) → False
checkConstrExp(Error(e11, e12), Bsf(op2, b21, b22)) → False
checkConstrExp(Error(e11, e12), Var(v2)) → False
checkConstrExp(F, Error(e21, e22)) → False
checkConstrExp(F, F) → True
checkConstrExp(F, T) → False
checkConstrExp(F, Fun(fn2, fe2)) → False
checkConstrExp(F, Eq(eq21, eq22)) → False
checkConstrExp(F, ITE'(i2, t2, e2)) → False
checkConstrExp(F, Bsf(op2, b21, b22)) → False
checkConstrExp(F, Var(v2)) → False
checkConstrExp(T, Error(e21, e22)) → False
checkConstrExp(T, F) → False
checkConstrExp(T, T) → True
checkConstrExp(T, Fun(fn2, fe2)) → False
checkConstrExp(T, Eq(eq21, eq22)) → False
checkConstrExp(T, ITE'(i2, t2, e2)) → False
checkConstrExp(T, Bsf(op2, b21, b22)) → False
checkConstrExp(T, Var(v2)) → False
checkConstrExp(Fun(fn1, fe1), Error(e21, e22)) → False
checkConstrExp(Fun(fn1, fe1), F) → False
checkConstrExp(Fun(fn1, fe1), T) → False
checkConstrExp(Fun(fn1, fe1), Fun(fn2, fe2)) → True
checkConstrExp(Fun(fn1, fe1), Eq(eq21, eq22)) → False
checkConstrExp(Fun(fn1, fe1), ITE'(i2, t2, e2)) → False
checkConstrExp(Fun(fn1, fe1), Bsf(op2, b21, b22)) → False
checkConstrExp(Fun(fn1, fe1), Var(v2)) → False
checkConstrExp(Eq(eq11, eq12), Error(e21, e22)) → False
checkConstrExp(Eq(eq11, eq12), F) → False
checkConstrExp(Eq(eq11, eq12), T) → False
checkConstrExp(Eq(eq11, eq12), Fun(fn2, fe2)) → False
checkConstrExp(Eq(eq11, eq12), Eq(eq21, eq22)) → True
checkConstrExp(Eq(eq11, eq12), ITE'(i2, t2, e2)) → False
checkConstrExp(Eq(eq11, eq12), Bsf(op2, b21, b22)) → False
checkConstrExp(Eq(eq11, eq12), Var(v2)) → False
checkConstrExp(ITE'(i1, t1, e1), Error(e21, e22)) → False
checkConstrExp(ITE'(i1, t1, e1), F) → False
checkConstrExp(ITE'(i1, t1, e1), T) → False
checkConstrExp(ITE'(i1, t1, e1), Fun(fn2, fe2)) → False
checkConstrExp(ITE'(i1, t1, e1), Eq(eq21, eq22)) → False
checkConstrExp(ITE'(i1, t1, e1), ITE'(i2, t2, e2)) → True
checkConstrExp(ITE'(i1, t1, e1), Bsf(op2, b21, b22)) → False
checkConstrExp(ITE'(i1, t1, e1), Var(v2)) → False
checkConstrExp(Bsf(op1, b11, b12), Error(e21, e22)) → False
checkConstrExp(Bsf(op1, b11, b12), F) → False
checkConstrExp(Bsf(op1, b11, b12), T) → False
checkConstrExp(Bsf(op1, b11, b12), Fun(fn2, fe2)) → False
checkConstrExp(Bsf(op1, b11, b12), Eq(eq21, eq22)) → False
checkConstrExp(Bsf(op1, b11, b12), ITE'(i2, t2, e2)) → False
checkConstrExp(Bsf(op1, b11, b12), Bsf(op2, b21, b22)) → True
checkConstrExp(Bsf(op1, b11, b12), Var(v2)) → False
checkConstrExp(Var(v1), Error(e21, e22)) → False
checkConstrExp(Var(v1), F) → False
checkConstrExp(Var(v1), T) → False
checkConstrExp(Var(v1), Fun(fn2, fe2)) → False
checkConstrExp(Var(v1), Eq(eq21, eq22)) → False
checkConstrExp(Var(v1), ITE'(i2, t2, e2)) → False
checkConstrExp(Var(v1), Bsf(op2, b21, b22)) → False
checkConstrExp(Var(v1), Var(v2)) → True
lookname(f, Cons(Fun(n, e), xs)) → lookname[Ite](!EQ(f, n), f, Cons(Fun(n, e), xs))
lookbody(f, Cons(Fun(n, e), xs)) → lookbody[Ite](!EQ(f, n), f, Cons(Fun(n, e), xs))
getVar(Var(int)) → int
getIfTrue(ITE'(i, t, e)) → t
getIfGuard(ITE'(i, t, e)) → i
getIfFalse(ITE'(i, t, e)) → e
getFuncName(Fun(n, e)) → n
getFuncExp(Fun(n, e)) → e
getEqSecond(Eq(f, s)) → s
getEqFirst(Eq(f, s)) → f
getConst(Cst(int)) → int
getBsfSecondTerm(Bsf(op, t1, t2)) → t2
getBsfOp(Bsf(op, t1, t2)) → op
getBsfFirstTerm(Bsf(op, t1, t2)) → t1
apply(op, v1, v2) → apply[Ite](eqExp(v1, v2), op, v1, v2)
lookvar(x', Cons(x, xs), vs) → lookvar[Ite](!EQ(x', x), x', Cons(x, xs), vs)
eqOps(o1, o2) → True
The (relative) TRS S consists of the following rules:
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
eeval[False][Ite](True, Eq(f, s), ns, vs, p) → eeval[True][Ite](eqExp(eeval(f, ns, vs, p), eeval(s, ns, vs, p)), Eq(f, s), ns, vs, p)
lookvar[Ite](False, x', Cons(x'', xs'), Cons(x, xs)) → lookvar(x', xs', xs)
lookname[Ite](True, f, Cons(Fun(n, e), xs)) → n
lookbody[Ite](True, f, Cons(Fun(n, e), xs)) → e
eeval[False][Ite](False, Fun(n, e), ns, vs, p) → eeval[False][Let](Fun(n, e), ns, vs, p, lookbody(n, p))
eeval[Ite](False, ITE'(i, t, e), ns, vs, p) → eeval(e, ns, vs, p)
eeval[Ite](True, ITE'(i, t, e), ns, vs, p) → eeval(t, ns, vs, p)
eeval[False][Let](Fun(n, e), ns, vs, p, ef) → eeval[False][Let][Let](Fun(n, e), ns, vs, p, ef, lookname(n, p))
eeval[False][Let][Let](Fun(n, e), ns, vs, p, ef, nf) → eeval[Let][Let][Let](Fun(n, e), ns, vs, p, ef, nf, eeval(e, ns, vs, p))
eeval[Let](Bsf(op, t1, t2), ns, vs, p, v1) → eeval[Let][Let](Bsf(op, t1, t2), ns, vs, p, v1, eeval(t2, ns, vs, p))
eeval[Let][Let](Bsf(op, t1, t2), ns, vs, p, v1, v2) → apply(op, v1, v2)
lookvar[Ite](True, x', ns, Cons(x, xs)) → x
lookname[Ite](False, f, Cons(x, xs)) → lookname(f, xs)
lookbody[Ite](False, f, Cons(x, xs)) → lookbody(f, xs)
eeval[True][Ite](False, e, ns, vs, p) → F
eeval[True][Ite](True, e, ns, vs, p) → T
apply[Ite](False, op, v1, v2) → F
apply[Ite](True, op, v1, v2) → T
run[Let][Let](p, input, f0, ef) → run[Let](p, input, f0, ef, lookname(f0, p))
run[Let](p, input, f0, ef, nf) → eeval(ef, Cons(nf, Nil), Cons(input, Nil), p)
eeval[Let][Let][Let](e, ns, vs, p, ef, nf, v) → eeval(ef, Cons(nf, Nil), Cons(v, Nil), p)
Rewrite Strategy: INNERMOST
(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.
(6) Obligation:
Innermost TRS:
Rules:
eeval(Fun(n, e), ns, vs, p) → eeval[False][Let](Fun(n, e), ns, vs, p, lookbody(n, p))
eeval(Eq(f, s), ns, vs, p) → eeval[True][Ite](eqExp(eeval(f, ns, vs, p), eeval(s, ns, vs, p)), Eq(f, s), ns, vs, p)
eeval(Error(e11, e12), ns, vs, p) → eeval[False][Ite](False, Error(e11, e12), ns, vs, p)
eeval(F, ns, vs, p) → F
eeval(T, ns, vs, p) → T
eeval(ITE'(i, t, e), ns, vs, p) → eeval[Ite](checkConstrExp(eeval(i, ns, vs, p), T), ITE'(i, t, e), ns, vs, p)
eeval(Bsf(op, t1, t2), ns, vs, p) → eeval[Let](Bsf(op, t1, t2), ns, vs, p, eeval(t1, ns, vs, p))
eeval(Var(int), ns, vs, p) → lookvar(int, ns, vs)
run(Cons(Fun(f0, e), xs), input) → run[Let][Let](Cons(Fun(f0, e), xs), input, f0, lookbody(f0, Cons(Fun(f0, e), xs)))
eqExp(Error(e11, e12), Error(e21, e22)) → and(eqExp(e11, e21), eqExp(e12, e22))
eqExp(Error(e11, e12), F) → False
eqExp(Error(e11, e12), T) → False
eqExp(Error(e11, e12), Fun(fn2, fe2)) → False
eqExp(Error(e11, e12), Eq(eq21, eq22)) → False
eqExp(Error(e11, e12), ITE'(i2, t2, e2)) → False
eqExp(Error(e11, e12), Bsf(op2, b21, b22)) → False
eqExp(Error(e11, e12), Var(v2)) → False
eqExp(F, Error(e21, e22)) → False
eqExp(F, F) → True
eqExp(F, T) → False
eqExp(F, Fun(fn2, fe2)) → False
eqExp(F, Eq(eq21, eq22)) → False
eqExp(F, ITE'(i2, t2, e2)) → False
eqExp(F, Bsf(op2, b21, b22)) → False
eqExp(F, Var(v2)) → False
eqExp(T, Error(e21, e22)) → False
eqExp(T, F) → False
eqExp(T, T) → True
eqExp(T, Fun(fn2, fe2)) → False
eqExp(T, Eq(eq21, eq22)) → False
eqExp(T, ITE'(i2, t2, e2)) → False
eqExp(T, Bsf(op2, b21, b22)) → False
eqExp(T, Var(v2)) → False
eqExp(Fun(fn1, fe1), Error(e21, e22)) → False
eqExp(Fun(fn1, fe1), F) → False
eqExp(Fun(fn1, fe1), T) → False
eqExp(Fun(fn1, fe1), Fun(fn2, fe2)) → and(!EQ(fn1, fn2), eqExp(fe1, fe2))
eqExp(Fun(fn1, fe1), Eq(eq21, eq22)) → False
eqExp(Fun(fn1, fe1), ITE'(i2, t2, e2)) → False
eqExp(Fun(fn1, fe1), Bsf(op2, b21, b22)) → False
eqExp(Fun(fn1, fe1), Var(v2)) → False
eqExp(Eq(eq11, eq12), Error(e21, e22)) → False
eqExp(Eq(eq11, eq12), F) → False
eqExp(Eq(eq11, eq12), T) → False
eqExp(Eq(eq11, eq12), Fun(fn2, fe2)) → False
eqExp(Eq(eq11, eq12), Eq(eq21, eq22)) → and(eqExp(eq11, eq21), eqExp(eq12, eq22))
eqExp(Eq(eq11, eq12), ITE'(i2, t2, e2)) → False
eqExp(Eq(eq11, eq12), Bsf(op2, b21, b22)) → False
eqExp(Eq(eq11, eq12), Var(v2)) → False
eqExp(ITE'(i1, t1, e1), Error(e21, e22)) → False
eqExp(ITE'(i1, t1, e1), F) → False
eqExp(ITE'(i1, t1, e1), T) → False
eqExp(ITE'(i1, t1, e1), Fun(fn2, fe2)) → False
eqExp(ITE'(i1, t1, e1), Eq(eq21, eq22)) → False
eqExp(ITE'(i1, t1, e1), ITE'(i2, t2, e2)) → and(eqExp(i1, i2), and(eqExp(t1, t2), eqExp(e1, e2)))
eqExp(ITE'(i1, t1, e1), Bsf(op2, b21, b22)) → False
eqExp(ITE'(i1, t1, e1), Var(v2)) → False
eqExp(Bsf(op1, b11, b12), Error(e21, e22)) → False
eqExp(Bsf(op1, b11, b12), F) → False
eqExp(Bsf(op1, b11, b12), T) → False
eqExp(Bsf(op1, b11, b12), Fun(fn2, fe2)) → False
eqExp(Bsf(op1, b11, b12), Eq(eq21, eq22)) → False
eqExp(Bsf(op1, b11, b12), ITE'(i2, t2, e2)) → False
eqExp(Bsf(o1, b11, b12), Bsf(o2, b21, b22)) → and(True, and(eqExp(b11, b21), eqExp(b12, b22)))
eqExp(Bsf(op1, b11, b12), Var(v2)) → False
eqExp(Var(v1), Error(e21, e22)) → False
eqExp(Var(v1), F) → False
eqExp(Var(v1), T) → False
eqExp(Var(v1), Fun(fn2, fe2)) → False
eqExp(Var(v1), Eq(eq21, eq22)) → False
eqExp(Var(v1), ITE'(i2, t2, e2)) → False
eqExp(Var(v1), Bsf(op2, b21, b22)) → False
eqExp(Var(v1), Var(v2)) → !EQ(v1, v2)
checkConstrExp(Error(e11, e12), Error(e21, e22)) → True
checkConstrExp(Error(e11, e12), F) → False
checkConstrExp(Error(e11, e12), T) → False
checkConstrExp(Error(e11, e12), Fun(fn2, fe2)) → False
checkConstrExp(Error(e11, e12), Eq(eq21, eq22)) → False
checkConstrExp(Error(e11, e12), ITE'(i2, t2, e2)) → False
checkConstrExp(Error(e11, e12), Bsf(op2, b21, b22)) → False
checkConstrExp(Error(e11, e12), Var(v2)) → False
checkConstrExp(F, Error(e21, e22)) → False
checkConstrExp(F, F) → True
checkConstrExp(F, T) → False
checkConstrExp(F, Fun(fn2, fe2)) → False
checkConstrExp(F, Eq(eq21, eq22)) → False
checkConstrExp(F, ITE'(i2, t2, e2)) → False
checkConstrExp(F, Bsf(op2, b21, b22)) → False
checkConstrExp(F, Var(v2)) → False
checkConstrExp(T, Error(e21, e22)) → False
checkConstrExp(T, F) → False
checkConstrExp(T, T) → True
checkConstrExp(T, Fun(fn2, fe2)) → False
checkConstrExp(T, Eq(eq21, eq22)) → False
checkConstrExp(T, ITE'(i2, t2, e2)) → False
checkConstrExp(T, Bsf(op2, b21, b22)) → False
checkConstrExp(T, Var(v2)) → False
checkConstrExp(Fun(fn1, fe1), Error(e21, e22)) → False
checkConstrExp(Fun(fn1, fe1), F) → False
checkConstrExp(Fun(fn1, fe1), T) → False
checkConstrExp(Fun(fn1, fe1), Fun(fn2, fe2)) → True
checkConstrExp(Fun(fn1, fe1), Eq(eq21, eq22)) → False
checkConstrExp(Fun(fn1, fe1), ITE'(i2, t2, e2)) → False
checkConstrExp(Fun(fn1, fe1), Bsf(op2, b21, b22)) → False
checkConstrExp(Fun(fn1, fe1), Var(v2)) → False
checkConstrExp(Eq(eq11, eq12), Error(e21, e22)) → False
checkConstrExp(Eq(eq11, eq12), F) → False
checkConstrExp(Eq(eq11, eq12), T) → False
checkConstrExp(Eq(eq11, eq12), Fun(fn2, fe2)) → False
checkConstrExp(Eq(eq11, eq12), Eq(eq21, eq22)) → True
checkConstrExp(Eq(eq11, eq12), ITE'(i2, t2, e2)) → False
checkConstrExp(Eq(eq11, eq12), Bsf(op2, b21, b22)) → False
checkConstrExp(Eq(eq11, eq12), Var(v2)) → False
checkConstrExp(ITE'(i1, t1, e1), Error(e21, e22)) → False
checkConstrExp(ITE'(i1, t1, e1), F) → False
checkConstrExp(ITE'(i1, t1, e1), T) → False
checkConstrExp(ITE'(i1, t1, e1), Fun(fn2, fe2)) → False
checkConstrExp(ITE'(i1, t1, e1), Eq(eq21, eq22)) → False
checkConstrExp(ITE'(i1, t1, e1), ITE'(i2, t2, e2)) → True
checkConstrExp(ITE'(i1, t1, e1), Bsf(op2, b21, b22)) → False
checkConstrExp(ITE'(i1, t1, e1), Var(v2)) → False
checkConstrExp(Bsf(op1, b11, b12), Error(e21, e22)) → False
checkConstrExp(Bsf(op1, b11, b12), F) → False
checkConstrExp(Bsf(op1, b11, b12), T) → False
checkConstrExp(Bsf(op1, b11, b12), Fun(fn2, fe2)) → False
checkConstrExp(Bsf(op1, b11, b12), Eq(eq21, eq22)) → False
checkConstrExp(Bsf(op1, b11, b12), ITE'(i2, t2, e2)) → False
checkConstrExp(Bsf(op1, b11, b12), Bsf(op2, b21, b22)) → True
checkConstrExp(Bsf(op1, b11, b12), Var(v2)) → False
checkConstrExp(Var(v1), Error(e21, e22)) → False
checkConstrExp(Var(v1), F) → False
checkConstrExp(Var(v1), T) → False
checkConstrExp(Var(v1), Fun(fn2, fe2)) → False
checkConstrExp(Var(v1), Eq(eq21, eq22)) → False
checkConstrExp(Var(v1), ITE'(i2, t2, e2)) → False
checkConstrExp(Var(v1), Bsf(op2, b21, b22)) → False
checkConstrExp(Var(v1), Var(v2)) → True
lookname(f, Cons(Fun(n, e), xs)) → lookname[Ite](!EQ(f, n), f, Cons(Fun(n, e), xs))
lookbody(f, Cons(Fun(n, e), xs)) → lookbody[Ite](!EQ(f, n), f, Cons(Fun(n, e), xs))
getVar(Var(int)) → int
getIfTrue(ITE'(i, t, e)) → t
getIfGuard(ITE'(i, t, e)) → i
getIfFalse(ITE'(i, t, e)) → e
getFuncName(Fun(n, e)) → n
getFuncExp(Fun(n, e)) → e
getEqSecond(Eq(f, s)) → s
getEqFirst(Eq(f, s)) → f
getConst(Cst(int)) → int
getBsfSecondTerm(Bsf(op, t1, t2)) → t2
getBsfOp(Bsf(op, t1, t2)) → op
getBsfFirstTerm(Bsf(op, t1, t2)) → t1
apply(op, v1, v2) → apply[Ite](eqExp(v1, v2), op, v1, v2)
lookvar(x', Cons(x, xs), vs) → lookvar[Ite](!EQ(x', x), x', Cons(x, xs), vs)
eqOps(o1, o2) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
eeval[False][Ite](True, Eq(f, s), ns, vs, p) → eeval[True][Ite](eqExp(eeval(f, ns, vs, p), eeval(s, ns, vs, p)), Eq(f, s), ns, vs, p)
lookvar[Ite](False, x', Cons(x'', xs'), Cons(x, xs)) → lookvar(x', xs', xs)
lookname[Ite](True, f, Cons(Fun(n, e), xs)) → n
lookbody[Ite](True, f, Cons(Fun(n, e), xs)) → e
eeval[False][Ite](False, Fun(n, e), ns, vs, p) → eeval[False][Let](Fun(n, e), ns, vs, p, lookbody(n, p))
eeval[Ite](False, ITE'(i, t, e), ns, vs, p) → eeval(e, ns, vs, p)
eeval[Ite](True, ITE'(i, t, e), ns, vs, p) → eeval(t, ns, vs, p)
eeval[False][Let](Fun(n, e), ns, vs, p, ef) → eeval[False][Let][Let](Fun(n, e), ns, vs, p, ef, lookname(n, p))
eeval[False][Let][Let](Fun(n, e), ns, vs, p, ef, nf) → eeval[Let][Let][Let](Fun(n, e), ns, vs, p, ef, nf, eeval(e, ns, vs, p))
eeval[Let](Bsf(op, t1, t2), ns, vs, p, v1) → eeval[Let][Let](Bsf(op, t1, t2), ns, vs, p, v1, eeval(t2, ns, vs, p))
eeval[Let][Let](Bsf(op, t1, t2), ns, vs, p, v1, v2) → apply(op, v1, v2)
lookvar[Ite](True, x', ns, Cons(x, xs)) → x
lookname[Ite](False, f, Cons(x, xs)) → lookname(f, xs)
lookbody[Ite](False, f, Cons(x, xs)) → lookbody(f, xs)
eeval[True][Ite](False, e, ns, vs, p) → F
eeval[True][Ite](True, e, ns, vs, p) → T
apply[Ite](False, op, v1, v2) → F
apply[Ite](True, op, v1, v2) → T
run[Let][Let](p, input, f0, ef) → run[Let](p, input, f0, ef, lookname(f0, p))
run[Let](p, input, f0, ef, nf) → eeval(ef, Cons(nf, Nil), Cons(input, Nil), p)
eeval[Let][Let][Let](e, ns, vs, p, ef, nf, v) → eeval(ef, Cons(nf, Nil), Cons(v, Nil), p)
Types:
eeval :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
Fun :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[False][Let] :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
lookbody :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
Eq :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[True][Ite] :: False:True → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eqExp :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → False:True
Error :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[False][Ite] :: False:True → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
False :: False:True
F :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
T :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
ITE' :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[Ite] :: False:True → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
checkConstrExp :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → False:True
Bsf :: getBsfOp → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[Let] :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
Var :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
lookvar :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
run :: Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
Cons :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil
run[Let][Let] :: Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
and :: False:True → False:True → False:True
True :: False:True
!EQ :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → False:True
lookname :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
lookname[Ite] :: False:True → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
lookbody[Ite] :: False:True → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getVar :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getIfTrue :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getIfGuard :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getIfFalse :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getFuncName :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getFuncExp :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getEqSecond :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getEqFirst :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getConst :: Cst → getConst
Cst :: getConst → Cst
getBsfSecondTerm :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getBsfOp :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → getBsfOp
getBsfFirstTerm :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
apply :: getBsfOp → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
apply[Ite] :: False:True → getBsfOp → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
lookvar[Ite] :: False:True → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eqOps :: a → b → False:True
S :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
0' :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[False][Let][Let] :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[Let][Let][Let] :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[Let][Let] :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
run[Let] :: Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
Nil :: Cons:Nil
hole_Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'1_3 :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
hole_Cons:Nil2_3 :: Cons:Nil
hole_False:True3_3 :: False:True
hole_getBsfOp4_3 :: getBsfOp
hole_getConst5_3 :: getConst
hole_Cst6_3 :: Cst
hole_a7_3 :: a
hole_b8_3 :: b
gen_Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'9_3 :: Nat → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
gen_Cons:Nil10_3 :: Nat → Cons:Nil
(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
eeval, eeval[False][Let], lookbody, eqExp, lookvar, !EQ, looknameThey will be analysed ascendingly in the following order:
eeval = eeval[False][Let]
lookbody < eeval
eqExp < eeval
lookvar < eeval
lookname < eeval[False][Let]
!EQ < lookbody
!EQ < eqExp
!EQ < lookvar
!EQ < lookname
(8) Obligation:
Innermost TRS:
Rules:
eeval(Fun(n, e), ns, vs, p) → eeval[False][Let](Fun(n, e), ns, vs, p, lookbody(n, p))
eeval(Eq(f, s), ns, vs, p) → eeval[True][Ite](eqExp(eeval(f, ns, vs, p), eeval(s, ns, vs, p)), Eq(f, s), ns, vs, p)
eeval(Error(e11, e12), ns, vs, p) → eeval[False][Ite](False, Error(e11, e12), ns, vs, p)
eeval(F, ns, vs, p) → F
eeval(T, ns, vs, p) → T
eeval(ITE'(i, t, e), ns, vs, p) → eeval[Ite](checkConstrExp(eeval(i, ns, vs, p), T), ITE'(i, t, e), ns, vs, p)
eeval(Bsf(op, t1, t2), ns, vs, p) → eeval[Let](Bsf(op, t1, t2), ns, vs, p, eeval(t1, ns, vs, p))
eeval(Var(int), ns, vs, p) → lookvar(int, ns, vs)
run(Cons(Fun(f0, e), xs), input) → run[Let][Let](Cons(Fun(f0, e), xs), input, f0, lookbody(f0, Cons(Fun(f0, e), xs)))
eqExp(Error(e11, e12), Error(e21, e22)) → and(eqExp(e11, e21), eqExp(e12, e22))
eqExp(Error(e11, e12), F) → False
eqExp(Error(e11, e12), T) → False
eqExp(Error(e11, e12), Fun(fn2, fe2)) → False
eqExp(Error(e11, e12), Eq(eq21, eq22)) → False
eqExp(Error(e11, e12), ITE'(i2, t2, e2)) → False
eqExp(Error(e11, e12), Bsf(op2, b21, b22)) → False
eqExp(Error(e11, e12), Var(v2)) → False
eqExp(F, Error(e21, e22)) → False
eqExp(F, F) → True
eqExp(F, T) → False
eqExp(F, Fun(fn2, fe2)) → False
eqExp(F, Eq(eq21, eq22)) → False
eqExp(F, ITE'(i2, t2, e2)) → False
eqExp(F, Bsf(op2, b21, b22)) → False
eqExp(F, Var(v2)) → False
eqExp(T, Error(e21, e22)) → False
eqExp(T, F) → False
eqExp(T, T) → True
eqExp(T, Fun(fn2, fe2)) → False
eqExp(T, Eq(eq21, eq22)) → False
eqExp(T, ITE'(i2, t2, e2)) → False
eqExp(T, Bsf(op2, b21, b22)) → False
eqExp(T, Var(v2)) → False
eqExp(Fun(fn1, fe1), Error(e21, e22)) → False
eqExp(Fun(fn1, fe1), F) → False
eqExp(Fun(fn1, fe1), T) → False
eqExp(Fun(fn1, fe1), Fun(fn2, fe2)) → and(!EQ(fn1, fn2), eqExp(fe1, fe2))
eqExp(Fun(fn1, fe1), Eq(eq21, eq22)) → False
eqExp(Fun(fn1, fe1), ITE'(i2, t2, e2)) → False
eqExp(Fun(fn1, fe1), Bsf(op2, b21, b22)) → False
eqExp(Fun(fn1, fe1), Var(v2)) → False
eqExp(Eq(eq11, eq12), Error(e21, e22)) → False
eqExp(Eq(eq11, eq12), F) → False
eqExp(Eq(eq11, eq12), T) → False
eqExp(Eq(eq11, eq12), Fun(fn2, fe2)) → False
eqExp(Eq(eq11, eq12), Eq(eq21, eq22)) → and(eqExp(eq11, eq21), eqExp(eq12, eq22))
eqExp(Eq(eq11, eq12), ITE'(i2, t2, e2)) → False
eqExp(Eq(eq11, eq12), Bsf(op2, b21, b22)) → False
eqExp(Eq(eq11, eq12), Var(v2)) → False
eqExp(ITE'(i1, t1, e1), Error(e21, e22)) → False
eqExp(ITE'(i1, t1, e1), F) → False
eqExp(ITE'(i1, t1, e1), T) → False
eqExp(ITE'(i1, t1, e1), Fun(fn2, fe2)) → False
eqExp(ITE'(i1, t1, e1), Eq(eq21, eq22)) → False
eqExp(ITE'(i1, t1, e1), ITE'(i2, t2, e2)) → and(eqExp(i1, i2), and(eqExp(t1, t2), eqExp(e1, e2)))
eqExp(ITE'(i1, t1, e1), Bsf(op2, b21, b22)) → False
eqExp(ITE'(i1, t1, e1), Var(v2)) → False
eqExp(Bsf(op1, b11, b12), Error(e21, e22)) → False
eqExp(Bsf(op1, b11, b12), F) → False
eqExp(Bsf(op1, b11, b12), T) → False
eqExp(Bsf(op1, b11, b12), Fun(fn2, fe2)) → False
eqExp(Bsf(op1, b11, b12), Eq(eq21, eq22)) → False
eqExp(Bsf(op1, b11, b12), ITE'(i2, t2, e2)) → False
eqExp(Bsf(o1, b11, b12), Bsf(o2, b21, b22)) → and(True, and(eqExp(b11, b21), eqExp(b12, b22)))
eqExp(Bsf(op1, b11, b12), Var(v2)) → False
eqExp(Var(v1), Error(e21, e22)) → False
eqExp(Var(v1), F) → False
eqExp(Var(v1), T) → False
eqExp(Var(v1), Fun(fn2, fe2)) → False
eqExp(Var(v1), Eq(eq21, eq22)) → False
eqExp(Var(v1), ITE'(i2, t2, e2)) → False
eqExp(Var(v1), Bsf(op2, b21, b22)) → False
eqExp(Var(v1), Var(v2)) → !EQ(v1, v2)
checkConstrExp(Error(e11, e12), Error(e21, e22)) → True
checkConstrExp(Error(e11, e12), F) → False
checkConstrExp(Error(e11, e12), T) → False
checkConstrExp(Error(e11, e12), Fun(fn2, fe2)) → False
checkConstrExp(Error(e11, e12), Eq(eq21, eq22)) → False
checkConstrExp(Error(e11, e12), ITE'(i2, t2, e2)) → False
checkConstrExp(Error(e11, e12), Bsf(op2, b21, b22)) → False
checkConstrExp(Error(e11, e12), Var(v2)) → False
checkConstrExp(F, Error(e21, e22)) → False
checkConstrExp(F, F) → True
checkConstrExp(F, T) → False
checkConstrExp(F, Fun(fn2, fe2)) → False
checkConstrExp(F, Eq(eq21, eq22)) → False
checkConstrExp(F, ITE'(i2, t2, e2)) → False
checkConstrExp(F, Bsf(op2, b21, b22)) → False
checkConstrExp(F, Var(v2)) → False
checkConstrExp(T, Error(e21, e22)) → False
checkConstrExp(T, F) → False
checkConstrExp(T, T) → True
checkConstrExp(T, Fun(fn2, fe2)) → False
checkConstrExp(T, Eq(eq21, eq22)) → False
checkConstrExp(T, ITE'(i2, t2, e2)) → False
checkConstrExp(T, Bsf(op2, b21, b22)) → False
checkConstrExp(T, Var(v2)) → False
checkConstrExp(Fun(fn1, fe1), Error(e21, e22)) → False
checkConstrExp(Fun(fn1, fe1), F) → False
checkConstrExp(Fun(fn1, fe1), T) → False
checkConstrExp(Fun(fn1, fe1), Fun(fn2, fe2)) → True
checkConstrExp(Fun(fn1, fe1), Eq(eq21, eq22)) → False
checkConstrExp(Fun(fn1, fe1), ITE'(i2, t2, e2)) → False
checkConstrExp(Fun(fn1, fe1), Bsf(op2, b21, b22)) → False
checkConstrExp(Fun(fn1, fe1), Var(v2)) → False
checkConstrExp(Eq(eq11, eq12), Error(e21, e22)) → False
checkConstrExp(Eq(eq11, eq12), F) → False
checkConstrExp(Eq(eq11, eq12), T) → False
checkConstrExp(Eq(eq11, eq12), Fun(fn2, fe2)) → False
checkConstrExp(Eq(eq11, eq12), Eq(eq21, eq22)) → True
checkConstrExp(Eq(eq11, eq12), ITE'(i2, t2, e2)) → False
checkConstrExp(Eq(eq11, eq12), Bsf(op2, b21, b22)) → False
checkConstrExp(Eq(eq11, eq12), Var(v2)) → False
checkConstrExp(ITE'(i1, t1, e1), Error(e21, e22)) → False
checkConstrExp(ITE'(i1, t1, e1), F) → False
checkConstrExp(ITE'(i1, t1, e1), T) → False
checkConstrExp(ITE'(i1, t1, e1), Fun(fn2, fe2)) → False
checkConstrExp(ITE'(i1, t1, e1), Eq(eq21, eq22)) → False
checkConstrExp(ITE'(i1, t1, e1), ITE'(i2, t2, e2)) → True
checkConstrExp(ITE'(i1, t1, e1), Bsf(op2, b21, b22)) → False
checkConstrExp(ITE'(i1, t1, e1), Var(v2)) → False
checkConstrExp(Bsf(op1, b11, b12), Error(e21, e22)) → False
checkConstrExp(Bsf(op1, b11, b12), F) → False
checkConstrExp(Bsf(op1, b11, b12), T) → False
checkConstrExp(Bsf(op1, b11, b12), Fun(fn2, fe2)) → False
checkConstrExp(Bsf(op1, b11, b12), Eq(eq21, eq22)) → False
checkConstrExp(Bsf(op1, b11, b12), ITE'(i2, t2, e2)) → False
checkConstrExp(Bsf(op1, b11, b12), Bsf(op2, b21, b22)) → True
checkConstrExp(Bsf(op1, b11, b12), Var(v2)) → False
checkConstrExp(Var(v1), Error(e21, e22)) → False
checkConstrExp(Var(v1), F) → False
checkConstrExp(Var(v1), T) → False
checkConstrExp(Var(v1), Fun(fn2, fe2)) → False
checkConstrExp(Var(v1), Eq(eq21, eq22)) → False
checkConstrExp(Var(v1), ITE'(i2, t2, e2)) → False
checkConstrExp(Var(v1), Bsf(op2, b21, b22)) → False
checkConstrExp(Var(v1), Var(v2)) → True
lookname(f, Cons(Fun(n, e), xs)) → lookname[Ite](!EQ(f, n), f, Cons(Fun(n, e), xs))
lookbody(f, Cons(Fun(n, e), xs)) → lookbody[Ite](!EQ(f, n), f, Cons(Fun(n, e), xs))
getVar(Var(int)) → int
getIfTrue(ITE'(i, t, e)) → t
getIfGuard(ITE'(i, t, e)) → i
getIfFalse(ITE'(i, t, e)) → e
getFuncName(Fun(n, e)) → n
getFuncExp(Fun(n, e)) → e
getEqSecond(Eq(f, s)) → s
getEqFirst(Eq(f, s)) → f
getConst(Cst(int)) → int
getBsfSecondTerm(Bsf(op, t1, t2)) → t2
getBsfOp(Bsf(op, t1, t2)) → op
getBsfFirstTerm(Bsf(op, t1, t2)) → t1
apply(op, v1, v2) → apply[Ite](eqExp(v1, v2), op, v1, v2)
lookvar(x', Cons(x, xs), vs) → lookvar[Ite](!EQ(x', x), x', Cons(x, xs), vs)
eqOps(o1, o2) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
eeval[False][Ite](True, Eq(f, s), ns, vs, p) → eeval[True][Ite](eqExp(eeval(f, ns, vs, p), eeval(s, ns, vs, p)), Eq(f, s), ns, vs, p)
lookvar[Ite](False, x', Cons(x'', xs'), Cons(x, xs)) → lookvar(x', xs', xs)
lookname[Ite](True, f, Cons(Fun(n, e), xs)) → n
lookbody[Ite](True, f, Cons(Fun(n, e), xs)) → e
eeval[False][Ite](False, Fun(n, e), ns, vs, p) → eeval[False][Let](Fun(n, e), ns, vs, p, lookbody(n, p))
eeval[Ite](False, ITE'(i, t, e), ns, vs, p) → eeval(e, ns, vs, p)
eeval[Ite](True, ITE'(i, t, e), ns, vs, p) → eeval(t, ns, vs, p)
eeval[False][Let](Fun(n, e), ns, vs, p, ef) → eeval[False][Let][Let](Fun(n, e), ns, vs, p, ef, lookname(n, p))
eeval[False][Let][Let](Fun(n, e), ns, vs, p, ef, nf) → eeval[Let][Let][Let](Fun(n, e), ns, vs, p, ef, nf, eeval(e, ns, vs, p))
eeval[Let](Bsf(op, t1, t2), ns, vs, p, v1) → eeval[Let][Let](Bsf(op, t1, t2), ns, vs, p, v1, eeval(t2, ns, vs, p))
eeval[Let][Let](Bsf(op, t1, t2), ns, vs, p, v1, v2) → apply(op, v1, v2)
lookvar[Ite](True, x', ns, Cons(x, xs)) → x
lookname[Ite](False, f, Cons(x, xs)) → lookname(f, xs)
lookbody[Ite](False, f, Cons(x, xs)) → lookbody(f, xs)
eeval[True][Ite](False, e, ns, vs, p) → F
eeval[True][Ite](True, e, ns, vs, p) → T
apply[Ite](False, op, v1, v2) → F
apply[Ite](True, op, v1, v2) → T
run[Let][Let](p, input, f0, ef) → run[Let](p, input, f0, ef, lookname(f0, p))
run[Let](p, input, f0, ef, nf) → eeval(ef, Cons(nf, Nil), Cons(input, Nil), p)
eeval[Let][Let][Let](e, ns, vs, p, ef, nf, v) → eeval(ef, Cons(nf, Nil), Cons(v, Nil), p)
Types:
eeval :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
Fun :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[False][Let] :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
lookbody :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
Eq :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[True][Ite] :: False:True → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eqExp :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → False:True
Error :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[False][Ite] :: False:True → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
False :: False:True
F :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
T :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
ITE' :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[Ite] :: False:True → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
checkConstrExp :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → False:True
Bsf :: getBsfOp → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[Let] :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
Var :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
lookvar :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
run :: Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
Cons :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil
run[Let][Let] :: Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
and :: False:True → False:True → False:True
True :: False:True
!EQ :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → False:True
lookname :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
lookname[Ite] :: False:True → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
lookbody[Ite] :: False:True → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getVar :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getIfTrue :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getIfGuard :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getIfFalse :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getFuncName :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getFuncExp :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getEqSecond :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getEqFirst :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getConst :: Cst → getConst
Cst :: getConst → Cst
getBsfSecondTerm :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getBsfOp :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → getBsfOp
getBsfFirstTerm :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
apply :: getBsfOp → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
apply[Ite] :: False:True → getBsfOp → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
lookvar[Ite] :: False:True → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eqOps :: a → b → False:True
S :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
0' :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[False][Let][Let] :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[Let][Let][Let] :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[Let][Let] :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
run[Let] :: Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
Nil :: Cons:Nil
hole_Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'1_3 :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
hole_Cons:Nil2_3 :: Cons:Nil
hole_False:True3_3 :: False:True
hole_getBsfOp4_3 :: getBsfOp
hole_getConst5_3 :: getConst
hole_Cst6_3 :: Cst
hole_a7_3 :: a
hole_b8_3 :: b
gen_Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'9_3 :: Nat → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
gen_Cons:Nil10_3 :: Nat → Cons:Nil
Generator Equations:
gen_Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'9_3(0) ⇔ F
gen_Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'9_3(+(x, 1)) ⇔ Fun(F, gen_Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'9_3(x))
gen_Cons:Nil10_3(0) ⇔ Nil
gen_Cons:Nil10_3(+(x, 1)) ⇔ Cons(F, gen_Cons:Nil10_3(x))
The following defined symbols remain to be analysed:
!EQ, eeval, eeval[False][Let], lookbody, eqExp, lookvar, lookname
They will be analysed ascendingly in the following order:
eeval = eeval[False][Let]
lookbody < eeval
eqExp < eeval
lookvar < eeval
lookname < eeval[False][Let]
!EQ < lookbody
!EQ < eqExp
!EQ < lookvar
!EQ < lookname
(9) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol !EQ.
(10) Obligation:
Innermost TRS:
Rules:
eeval(Fun(n, e), ns, vs, p) → eeval[False][Let](Fun(n, e), ns, vs, p, lookbody(n, p))
eeval(Eq(f, s), ns, vs, p) → eeval[True][Ite](eqExp(eeval(f, ns, vs, p), eeval(s, ns, vs, p)), Eq(f, s), ns, vs, p)
eeval(Error(e11, e12), ns, vs, p) → eeval[False][Ite](False, Error(e11, e12), ns, vs, p)
eeval(F, ns, vs, p) → F
eeval(T, ns, vs, p) → T
eeval(ITE'(i, t, e), ns, vs, p) → eeval[Ite](checkConstrExp(eeval(i, ns, vs, p), T), ITE'(i, t, e), ns, vs, p)
eeval(Bsf(op, t1, t2), ns, vs, p) → eeval[Let](Bsf(op, t1, t2), ns, vs, p, eeval(t1, ns, vs, p))
eeval(Var(int), ns, vs, p) → lookvar(int, ns, vs)
run(Cons(Fun(f0, e), xs), input) → run[Let][Let](Cons(Fun(f0, e), xs), input, f0, lookbody(f0, Cons(Fun(f0, e), xs)))
eqExp(Error(e11, e12), Error(e21, e22)) → and(eqExp(e11, e21), eqExp(e12, e22))
eqExp(Error(e11, e12), F) → False
eqExp(Error(e11, e12), T) → False
eqExp(Error(e11, e12), Fun(fn2, fe2)) → False
eqExp(Error(e11, e12), Eq(eq21, eq22)) → False
eqExp(Error(e11, e12), ITE'(i2, t2, e2)) → False
eqExp(Error(e11, e12), Bsf(op2, b21, b22)) → False
eqExp(Error(e11, e12), Var(v2)) → False
eqExp(F, Error(e21, e22)) → False
eqExp(F, F) → True
eqExp(F, T) → False
eqExp(F, Fun(fn2, fe2)) → False
eqExp(F, Eq(eq21, eq22)) → False
eqExp(F, ITE'(i2, t2, e2)) → False
eqExp(F, Bsf(op2, b21, b22)) → False
eqExp(F, Var(v2)) → False
eqExp(T, Error(e21, e22)) → False
eqExp(T, F) → False
eqExp(T, T) → True
eqExp(T, Fun(fn2, fe2)) → False
eqExp(T, Eq(eq21, eq22)) → False
eqExp(T, ITE'(i2, t2, e2)) → False
eqExp(T, Bsf(op2, b21, b22)) → False
eqExp(T, Var(v2)) → False
eqExp(Fun(fn1, fe1), Error(e21, e22)) → False
eqExp(Fun(fn1, fe1), F) → False
eqExp(Fun(fn1, fe1), T) → False
eqExp(Fun(fn1, fe1), Fun(fn2, fe2)) → and(!EQ(fn1, fn2), eqExp(fe1, fe2))
eqExp(Fun(fn1, fe1), Eq(eq21, eq22)) → False
eqExp(Fun(fn1, fe1), ITE'(i2, t2, e2)) → False
eqExp(Fun(fn1, fe1), Bsf(op2, b21, b22)) → False
eqExp(Fun(fn1, fe1), Var(v2)) → False
eqExp(Eq(eq11, eq12), Error(e21, e22)) → False
eqExp(Eq(eq11, eq12), F) → False
eqExp(Eq(eq11, eq12), T) → False
eqExp(Eq(eq11, eq12), Fun(fn2, fe2)) → False
eqExp(Eq(eq11, eq12), Eq(eq21, eq22)) → and(eqExp(eq11, eq21), eqExp(eq12, eq22))
eqExp(Eq(eq11, eq12), ITE'(i2, t2, e2)) → False
eqExp(Eq(eq11, eq12), Bsf(op2, b21, b22)) → False
eqExp(Eq(eq11, eq12), Var(v2)) → False
eqExp(ITE'(i1, t1, e1), Error(e21, e22)) → False
eqExp(ITE'(i1, t1, e1), F) → False
eqExp(ITE'(i1, t1, e1), T) → False
eqExp(ITE'(i1, t1, e1), Fun(fn2, fe2)) → False
eqExp(ITE'(i1, t1, e1), Eq(eq21, eq22)) → False
eqExp(ITE'(i1, t1, e1), ITE'(i2, t2, e2)) → and(eqExp(i1, i2), and(eqExp(t1, t2), eqExp(e1, e2)))
eqExp(ITE'(i1, t1, e1), Bsf(op2, b21, b22)) → False
eqExp(ITE'(i1, t1, e1), Var(v2)) → False
eqExp(Bsf(op1, b11, b12), Error(e21, e22)) → False
eqExp(Bsf(op1, b11, b12), F) → False
eqExp(Bsf(op1, b11, b12), T) → False
eqExp(Bsf(op1, b11, b12), Fun(fn2, fe2)) → False
eqExp(Bsf(op1, b11, b12), Eq(eq21, eq22)) → False
eqExp(Bsf(op1, b11, b12), ITE'(i2, t2, e2)) → False
eqExp(Bsf(o1, b11, b12), Bsf(o2, b21, b22)) → and(True, and(eqExp(b11, b21), eqExp(b12, b22)))
eqExp(Bsf(op1, b11, b12), Var(v2)) → False
eqExp(Var(v1), Error(e21, e22)) → False
eqExp(Var(v1), F) → False
eqExp(Var(v1), T) → False
eqExp(Var(v1), Fun(fn2, fe2)) → False
eqExp(Var(v1), Eq(eq21, eq22)) → False
eqExp(Var(v1), ITE'(i2, t2, e2)) → False
eqExp(Var(v1), Bsf(op2, b21, b22)) → False
eqExp(Var(v1), Var(v2)) → !EQ(v1, v2)
checkConstrExp(Error(e11, e12), Error(e21, e22)) → True
checkConstrExp(Error(e11, e12), F) → False
checkConstrExp(Error(e11, e12), T) → False
checkConstrExp(Error(e11, e12), Fun(fn2, fe2)) → False
checkConstrExp(Error(e11, e12), Eq(eq21, eq22)) → False
checkConstrExp(Error(e11, e12), ITE'(i2, t2, e2)) → False
checkConstrExp(Error(e11, e12), Bsf(op2, b21, b22)) → False
checkConstrExp(Error(e11, e12), Var(v2)) → False
checkConstrExp(F, Error(e21, e22)) → False
checkConstrExp(F, F) → True
checkConstrExp(F, T) → False
checkConstrExp(F, Fun(fn2, fe2)) → False
checkConstrExp(F, Eq(eq21, eq22)) → False
checkConstrExp(F, ITE'(i2, t2, e2)) → False
checkConstrExp(F, Bsf(op2, b21, b22)) → False
checkConstrExp(F, Var(v2)) → False
checkConstrExp(T, Error(e21, e22)) → False
checkConstrExp(T, F) → False
checkConstrExp(T, T) → True
checkConstrExp(T, Fun(fn2, fe2)) → False
checkConstrExp(T, Eq(eq21, eq22)) → False
checkConstrExp(T, ITE'(i2, t2, e2)) → False
checkConstrExp(T, Bsf(op2, b21, b22)) → False
checkConstrExp(T, Var(v2)) → False
checkConstrExp(Fun(fn1, fe1), Error(e21, e22)) → False
checkConstrExp(Fun(fn1, fe1), F) → False
checkConstrExp(Fun(fn1, fe1), T) → False
checkConstrExp(Fun(fn1, fe1), Fun(fn2, fe2)) → True
checkConstrExp(Fun(fn1, fe1), Eq(eq21, eq22)) → False
checkConstrExp(Fun(fn1, fe1), ITE'(i2, t2, e2)) → False
checkConstrExp(Fun(fn1, fe1), Bsf(op2, b21, b22)) → False
checkConstrExp(Fun(fn1, fe1), Var(v2)) → False
checkConstrExp(Eq(eq11, eq12), Error(e21, e22)) → False
checkConstrExp(Eq(eq11, eq12), F) → False
checkConstrExp(Eq(eq11, eq12), T) → False
checkConstrExp(Eq(eq11, eq12), Fun(fn2, fe2)) → False
checkConstrExp(Eq(eq11, eq12), Eq(eq21, eq22)) → True
checkConstrExp(Eq(eq11, eq12), ITE'(i2, t2, e2)) → False
checkConstrExp(Eq(eq11, eq12), Bsf(op2, b21, b22)) → False
checkConstrExp(Eq(eq11, eq12), Var(v2)) → False
checkConstrExp(ITE'(i1, t1, e1), Error(e21, e22)) → False
checkConstrExp(ITE'(i1, t1, e1), F) → False
checkConstrExp(ITE'(i1, t1, e1), T) → False
checkConstrExp(ITE'(i1, t1, e1), Fun(fn2, fe2)) → False
checkConstrExp(ITE'(i1, t1, e1), Eq(eq21, eq22)) → False
checkConstrExp(ITE'(i1, t1, e1), ITE'(i2, t2, e2)) → True
checkConstrExp(ITE'(i1, t1, e1), Bsf(op2, b21, b22)) → False
checkConstrExp(ITE'(i1, t1, e1), Var(v2)) → False
checkConstrExp(Bsf(op1, b11, b12), Error(e21, e22)) → False
checkConstrExp(Bsf(op1, b11, b12), F) → False
checkConstrExp(Bsf(op1, b11, b12), T) → False
checkConstrExp(Bsf(op1, b11, b12), Fun(fn2, fe2)) → False
checkConstrExp(Bsf(op1, b11, b12), Eq(eq21, eq22)) → False
checkConstrExp(Bsf(op1, b11, b12), ITE'(i2, t2, e2)) → False
checkConstrExp(Bsf(op1, b11, b12), Bsf(op2, b21, b22)) → True
checkConstrExp(Bsf(op1, b11, b12), Var(v2)) → False
checkConstrExp(Var(v1), Error(e21, e22)) → False
checkConstrExp(Var(v1), F) → False
checkConstrExp(Var(v1), T) → False
checkConstrExp(Var(v1), Fun(fn2, fe2)) → False
checkConstrExp(Var(v1), Eq(eq21, eq22)) → False
checkConstrExp(Var(v1), ITE'(i2, t2, e2)) → False
checkConstrExp(Var(v1), Bsf(op2, b21, b22)) → False
checkConstrExp(Var(v1), Var(v2)) → True
lookname(f, Cons(Fun(n, e), xs)) → lookname[Ite](!EQ(f, n), f, Cons(Fun(n, e), xs))
lookbody(f, Cons(Fun(n, e), xs)) → lookbody[Ite](!EQ(f, n), f, Cons(Fun(n, e), xs))
getVar(Var(int)) → int
getIfTrue(ITE'(i, t, e)) → t
getIfGuard(ITE'(i, t, e)) → i
getIfFalse(ITE'(i, t, e)) → e
getFuncName(Fun(n, e)) → n
getFuncExp(Fun(n, e)) → e
getEqSecond(Eq(f, s)) → s
getEqFirst(Eq(f, s)) → f
getConst(Cst(int)) → int
getBsfSecondTerm(Bsf(op, t1, t2)) → t2
getBsfOp(Bsf(op, t1, t2)) → op
getBsfFirstTerm(Bsf(op, t1, t2)) → t1
apply(op, v1, v2) → apply[Ite](eqExp(v1, v2), op, v1, v2)
lookvar(x', Cons(x, xs), vs) → lookvar[Ite](!EQ(x', x), x', Cons(x, xs), vs)
eqOps(o1, o2) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
eeval[False][Ite](True, Eq(f, s), ns, vs, p) → eeval[True][Ite](eqExp(eeval(f, ns, vs, p), eeval(s, ns, vs, p)), Eq(f, s), ns, vs, p)
lookvar[Ite](False, x', Cons(x'', xs'), Cons(x, xs)) → lookvar(x', xs', xs)
lookname[Ite](True, f, Cons(Fun(n, e), xs)) → n
lookbody[Ite](True, f, Cons(Fun(n, e), xs)) → e
eeval[False][Ite](False, Fun(n, e), ns, vs, p) → eeval[False][Let](Fun(n, e), ns, vs, p, lookbody(n, p))
eeval[Ite](False, ITE'(i, t, e), ns, vs, p) → eeval(e, ns, vs, p)
eeval[Ite](True, ITE'(i, t, e), ns, vs, p) → eeval(t, ns, vs, p)
eeval[False][Let](Fun(n, e), ns, vs, p, ef) → eeval[False][Let][Let](Fun(n, e), ns, vs, p, ef, lookname(n, p))
eeval[False][Let][Let](Fun(n, e), ns, vs, p, ef, nf) → eeval[Let][Let][Let](Fun(n, e), ns, vs, p, ef, nf, eeval(e, ns, vs, p))
eeval[Let](Bsf(op, t1, t2), ns, vs, p, v1) → eeval[Let][Let](Bsf(op, t1, t2), ns, vs, p, v1, eeval(t2, ns, vs, p))
eeval[Let][Let](Bsf(op, t1, t2), ns, vs, p, v1, v2) → apply(op, v1, v2)
lookvar[Ite](True, x', ns, Cons(x, xs)) → x
lookname[Ite](False, f, Cons(x, xs)) → lookname(f, xs)
lookbody[Ite](False, f, Cons(x, xs)) → lookbody(f, xs)
eeval[True][Ite](False, e, ns, vs, p) → F
eeval[True][Ite](True, e, ns, vs, p) → T
apply[Ite](False, op, v1, v2) → F
apply[Ite](True, op, v1, v2) → T
run[Let][Let](p, input, f0, ef) → run[Let](p, input, f0, ef, lookname(f0, p))
run[Let](p, input, f0, ef, nf) → eeval(ef, Cons(nf, Nil), Cons(input, Nil), p)
eeval[Let][Let][Let](e, ns, vs, p, ef, nf, v) → eeval(ef, Cons(nf, Nil), Cons(v, Nil), p)
Types:
eeval :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
Fun :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[False][Let] :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
lookbody :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
Eq :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[True][Ite] :: False:True → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eqExp :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → False:True
Error :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[False][Ite] :: False:True → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
False :: False:True
F :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
T :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
ITE' :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[Ite] :: False:True → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
checkConstrExp :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → False:True
Bsf :: getBsfOp → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[Let] :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
Var :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
lookvar :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
run :: Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
Cons :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil
run[Let][Let] :: Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
and :: False:True → False:True → False:True
True :: False:True
!EQ :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → False:True
lookname :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
lookname[Ite] :: False:True → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
lookbody[Ite] :: False:True → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getVar :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getIfTrue :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getIfGuard :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getIfFalse :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getFuncName :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getFuncExp :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getEqSecond :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getEqFirst :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getConst :: Cst → getConst
Cst :: getConst → Cst
getBsfSecondTerm :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getBsfOp :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → getBsfOp
getBsfFirstTerm :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
apply :: getBsfOp → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
apply[Ite] :: False:True → getBsfOp → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
lookvar[Ite] :: False:True → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eqOps :: a → b → False:True
S :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
0' :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[False][Let][Let] :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[Let][Let][Let] :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[Let][Let] :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
run[Let] :: Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
Nil :: Cons:Nil
hole_Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'1_3 :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
hole_Cons:Nil2_3 :: Cons:Nil
hole_False:True3_3 :: False:True
hole_getBsfOp4_3 :: getBsfOp
hole_getConst5_3 :: getConst
hole_Cst6_3 :: Cst
hole_a7_3 :: a
hole_b8_3 :: b
gen_Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'9_3 :: Nat → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
gen_Cons:Nil10_3 :: Nat → Cons:Nil
Generator Equations:
gen_Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'9_3(0) ⇔ F
gen_Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'9_3(+(x, 1)) ⇔ Fun(F, gen_Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'9_3(x))
gen_Cons:Nil10_3(0) ⇔ Nil
gen_Cons:Nil10_3(+(x, 1)) ⇔ Cons(F, gen_Cons:Nil10_3(x))
The following defined symbols remain to be analysed:
lookbody, eeval, eeval[False][Let], eqExp, lookvar, lookname
They will be analysed ascendingly in the following order:
eeval = eeval[False][Let]
lookbody < eeval
eqExp < eeval
lookvar < eeval
lookname < eeval[False][Let]
(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol lookbody.
(12) Obligation:
Innermost TRS:
Rules:
eeval(Fun(n, e), ns, vs, p) → eeval[False][Let](Fun(n, e), ns, vs, p, lookbody(n, p))
eeval(Eq(f, s), ns, vs, p) → eeval[True][Ite](eqExp(eeval(f, ns, vs, p), eeval(s, ns, vs, p)), Eq(f, s), ns, vs, p)
eeval(Error(e11, e12), ns, vs, p) → eeval[False][Ite](False, Error(e11, e12), ns, vs, p)
eeval(F, ns, vs, p) → F
eeval(T, ns, vs, p) → T
eeval(ITE'(i, t, e), ns, vs, p) → eeval[Ite](checkConstrExp(eeval(i, ns, vs, p), T), ITE'(i, t, e), ns, vs, p)
eeval(Bsf(op, t1, t2), ns, vs, p) → eeval[Let](Bsf(op, t1, t2), ns, vs, p, eeval(t1, ns, vs, p))
eeval(Var(int), ns, vs, p) → lookvar(int, ns, vs)
run(Cons(Fun(f0, e), xs), input) → run[Let][Let](Cons(Fun(f0, e), xs), input, f0, lookbody(f0, Cons(Fun(f0, e), xs)))
eqExp(Error(e11, e12), Error(e21, e22)) → and(eqExp(e11, e21), eqExp(e12, e22))
eqExp(Error(e11, e12), F) → False
eqExp(Error(e11, e12), T) → False
eqExp(Error(e11, e12), Fun(fn2, fe2)) → False
eqExp(Error(e11, e12), Eq(eq21, eq22)) → False
eqExp(Error(e11, e12), ITE'(i2, t2, e2)) → False
eqExp(Error(e11, e12), Bsf(op2, b21, b22)) → False
eqExp(Error(e11, e12), Var(v2)) → False
eqExp(F, Error(e21, e22)) → False
eqExp(F, F) → True
eqExp(F, T) → False
eqExp(F, Fun(fn2, fe2)) → False
eqExp(F, Eq(eq21, eq22)) → False
eqExp(F, ITE'(i2, t2, e2)) → False
eqExp(F, Bsf(op2, b21, b22)) → False
eqExp(F, Var(v2)) → False
eqExp(T, Error(e21, e22)) → False
eqExp(T, F) → False
eqExp(T, T) → True
eqExp(T, Fun(fn2, fe2)) → False
eqExp(T, Eq(eq21, eq22)) → False
eqExp(T, ITE'(i2, t2, e2)) → False
eqExp(T, Bsf(op2, b21, b22)) → False
eqExp(T, Var(v2)) → False
eqExp(Fun(fn1, fe1), Error(e21, e22)) → False
eqExp(Fun(fn1, fe1), F) → False
eqExp(Fun(fn1, fe1), T) → False
eqExp(Fun(fn1, fe1), Fun(fn2, fe2)) → and(!EQ(fn1, fn2), eqExp(fe1, fe2))
eqExp(Fun(fn1, fe1), Eq(eq21, eq22)) → False
eqExp(Fun(fn1, fe1), ITE'(i2, t2, e2)) → False
eqExp(Fun(fn1, fe1), Bsf(op2, b21, b22)) → False
eqExp(Fun(fn1, fe1), Var(v2)) → False
eqExp(Eq(eq11, eq12), Error(e21, e22)) → False
eqExp(Eq(eq11, eq12), F) → False
eqExp(Eq(eq11, eq12), T) → False
eqExp(Eq(eq11, eq12), Fun(fn2, fe2)) → False
eqExp(Eq(eq11, eq12), Eq(eq21, eq22)) → and(eqExp(eq11, eq21), eqExp(eq12, eq22))
eqExp(Eq(eq11, eq12), ITE'(i2, t2, e2)) → False
eqExp(Eq(eq11, eq12), Bsf(op2, b21, b22)) → False
eqExp(Eq(eq11, eq12), Var(v2)) → False
eqExp(ITE'(i1, t1, e1), Error(e21, e22)) → False
eqExp(ITE'(i1, t1, e1), F) → False
eqExp(ITE'(i1, t1, e1), T) → False
eqExp(ITE'(i1, t1, e1), Fun(fn2, fe2)) → False
eqExp(ITE'(i1, t1, e1), Eq(eq21, eq22)) → False
eqExp(ITE'(i1, t1, e1), ITE'(i2, t2, e2)) → and(eqExp(i1, i2), and(eqExp(t1, t2), eqExp(e1, e2)))
eqExp(ITE'(i1, t1, e1), Bsf(op2, b21, b22)) → False
eqExp(ITE'(i1, t1, e1), Var(v2)) → False
eqExp(Bsf(op1, b11, b12), Error(e21, e22)) → False
eqExp(Bsf(op1, b11, b12), F) → False
eqExp(Bsf(op1, b11, b12), T) → False
eqExp(Bsf(op1, b11, b12), Fun(fn2, fe2)) → False
eqExp(Bsf(op1, b11, b12), Eq(eq21, eq22)) → False
eqExp(Bsf(op1, b11, b12), ITE'(i2, t2, e2)) → False
eqExp(Bsf(o1, b11, b12), Bsf(o2, b21, b22)) → and(True, and(eqExp(b11, b21), eqExp(b12, b22)))
eqExp(Bsf(op1, b11, b12), Var(v2)) → False
eqExp(Var(v1), Error(e21, e22)) → False
eqExp(Var(v1), F) → False
eqExp(Var(v1), T) → False
eqExp(Var(v1), Fun(fn2, fe2)) → False
eqExp(Var(v1), Eq(eq21, eq22)) → False
eqExp(Var(v1), ITE'(i2, t2, e2)) → False
eqExp(Var(v1), Bsf(op2, b21, b22)) → False
eqExp(Var(v1), Var(v2)) → !EQ(v1, v2)
checkConstrExp(Error(e11, e12), Error(e21, e22)) → True
checkConstrExp(Error(e11, e12), F) → False
checkConstrExp(Error(e11, e12), T) → False
checkConstrExp(Error(e11, e12), Fun(fn2, fe2)) → False
checkConstrExp(Error(e11, e12), Eq(eq21, eq22)) → False
checkConstrExp(Error(e11, e12), ITE'(i2, t2, e2)) → False
checkConstrExp(Error(e11, e12), Bsf(op2, b21, b22)) → False
checkConstrExp(Error(e11, e12), Var(v2)) → False
checkConstrExp(F, Error(e21, e22)) → False
checkConstrExp(F, F) → True
checkConstrExp(F, T) → False
checkConstrExp(F, Fun(fn2, fe2)) → False
checkConstrExp(F, Eq(eq21, eq22)) → False
checkConstrExp(F, ITE'(i2, t2, e2)) → False
checkConstrExp(F, Bsf(op2, b21, b22)) → False
checkConstrExp(F, Var(v2)) → False
checkConstrExp(T, Error(e21, e22)) → False
checkConstrExp(T, F) → False
checkConstrExp(T, T) → True
checkConstrExp(T, Fun(fn2, fe2)) → False
checkConstrExp(T, Eq(eq21, eq22)) → False
checkConstrExp(T, ITE'(i2, t2, e2)) → False
checkConstrExp(T, Bsf(op2, b21, b22)) → False
checkConstrExp(T, Var(v2)) → False
checkConstrExp(Fun(fn1, fe1), Error(e21, e22)) → False
checkConstrExp(Fun(fn1, fe1), F) → False
checkConstrExp(Fun(fn1, fe1), T) → False
checkConstrExp(Fun(fn1, fe1), Fun(fn2, fe2)) → True
checkConstrExp(Fun(fn1, fe1), Eq(eq21, eq22)) → False
checkConstrExp(Fun(fn1, fe1), ITE'(i2, t2, e2)) → False
checkConstrExp(Fun(fn1, fe1), Bsf(op2, b21, b22)) → False
checkConstrExp(Fun(fn1, fe1), Var(v2)) → False
checkConstrExp(Eq(eq11, eq12), Error(e21, e22)) → False
checkConstrExp(Eq(eq11, eq12), F) → False
checkConstrExp(Eq(eq11, eq12), T) → False
checkConstrExp(Eq(eq11, eq12), Fun(fn2, fe2)) → False
checkConstrExp(Eq(eq11, eq12), Eq(eq21, eq22)) → True
checkConstrExp(Eq(eq11, eq12), ITE'(i2, t2, e2)) → False
checkConstrExp(Eq(eq11, eq12), Bsf(op2, b21, b22)) → False
checkConstrExp(Eq(eq11, eq12), Var(v2)) → False
checkConstrExp(ITE'(i1, t1, e1), Error(e21, e22)) → False
checkConstrExp(ITE'(i1, t1, e1), F) → False
checkConstrExp(ITE'(i1, t1, e1), T) → False
checkConstrExp(ITE'(i1, t1, e1), Fun(fn2, fe2)) → False
checkConstrExp(ITE'(i1, t1, e1), Eq(eq21, eq22)) → False
checkConstrExp(ITE'(i1, t1, e1), ITE'(i2, t2, e2)) → True
checkConstrExp(ITE'(i1, t1, e1), Bsf(op2, b21, b22)) → False
checkConstrExp(ITE'(i1, t1, e1), Var(v2)) → False
checkConstrExp(Bsf(op1, b11, b12), Error(e21, e22)) → False
checkConstrExp(Bsf(op1, b11, b12), F) → False
checkConstrExp(Bsf(op1, b11, b12), T) → False
checkConstrExp(Bsf(op1, b11, b12), Fun(fn2, fe2)) → False
checkConstrExp(Bsf(op1, b11, b12), Eq(eq21, eq22)) → False
checkConstrExp(Bsf(op1, b11, b12), ITE'(i2, t2, e2)) → False
checkConstrExp(Bsf(op1, b11, b12), Bsf(op2, b21, b22)) → True
checkConstrExp(Bsf(op1, b11, b12), Var(v2)) → False
checkConstrExp(Var(v1), Error(e21, e22)) → False
checkConstrExp(Var(v1), F) → False
checkConstrExp(Var(v1), T) → False
checkConstrExp(Var(v1), Fun(fn2, fe2)) → False
checkConstrExp(Var(v1), Eq(eq21, eq22)) → False
checkConstrExp(Var(v1), ITE'(i2, t2, e2)) → False
checkConstrExp(Var(v1), Bsf(op2, b21, b22)) → False
checkConstrExp(Var(v1), Var(v2)) → True
lookname(f, Cons(Fun(n, e), xs)) → lookname[Ite](!EQ(f, n), f, Cons(Fun(n, e), xs))
lookbody(f, Cons(Fun(n, e), xs)) → lookbody[Ite](!EQ(f, n), f, Cons(Fun(n, e), xs))
getVar(Var(int)) → int
getIfTrue(ITE'(i, t, e)) → t
getIfGuard(ITE'(i, t, e)) → i
getIfFalse(ITE'(i, t, e)) → e
getFuncName(Fun(n, e)) → n
getFuncExp(Fun(n, e)) → e
getEqSecond(Eq(f, s)) → s
getEqFirst(Eq(f, s)) → f
getConst(Cst(int)) → int
getBsfSecondTerm(Bsf(op, t1, t2)) → t2
getBsfOp(Bsf(op, t1, t2)) → op
getBsfFirstTerm(Bsf(op, t1, t2)) → t1
apply(op, v1, v2) → apply[Ite](eqExp(v1, v2), op, v1, v2)
lookvar(x', Cons(x, xs), vs) → lookvar[Ite](!EQ(x', x), x', Cons(x, xs), vs)
eqOps(o1, o2) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0', S(y)) → False
!EQ(S(x), 0') → False
!EQ(0', 0') → True
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
eeval[False][Ite](True, Eq(f, s), ns, vs, p) → eeval[True][Ite](eqExp(eeval(f, ns, vs, p), eeval(s, ns, vs, p)), Eq(f, s), ns, vs, p)
lookvar[Ite](False, x', Cons(x'', xs'), Cons(x, xs)) → lookvar(x', xs', xs)
lookname[Ite](True, f, Cons(Fun(n, e), xs)) → n
lookbody[Ite](True, f, Cons(Fun(n, e), xs)) → e
eeval[False][Ite](False, Fun(n, e), ns, vs, p) → eeval[False][Let](Fun(n, e), ns, vs, p, lookbody(n, p))
eeval[Ite](False, ITE'(i, t, e), ns, vs, p) → eeval(e, ns, vs, p)
eeval[Ite](True, ITE'(i, t, e), ns, vs, p) → eeval(t, ns, vs, p)
eeval[False][Let](Fun(n, e), ns, vs, p, ef) → eeval[False][Let][Let](Fun(n, e), ns, vs, p, ef, lookname(n, p))
eeval[False][Let][Let](Fun(n, e), ns, vs, p, ef, nf) → eeval[Let][Let][Let](Fun(n, e), ns, vs, p, ef, nf, eeval(e, ns, vs, p))
eeval[Let](Bsf(op, t1, t2), ns, vs, p, v1) → eeval[Let][Let](Bsf(op, t1, t2), ns, vs, p, v1, eeval(t2, ns, vs, p))
eeval[Let][Let](Bsf(op, t1, t2), ns, vs, p, v1, v2) → apply(op, v1, v2)
lookvar[Ite](True, x', ns, Cons(x, xs)) → x
lookname[Ite](False, f, Cons(x, xs)) → lookname(f, xs)
lookbody[Ite](False, f, Cons(x, xs)) → lookbody(f, xs)
eeval[True][Ite](False, e, ns, vs, p) → F
eeval[True][Ite](True, e, ns, vs, p) → T
apply[Ite](False, op, v1, v2) → F
apply[Ite](True, op, v1, v2) → T
run[Let][Let](p, input, f0, ef) → run[Let](p, input, f0, ef, lookname(f0, p))
run[Let](p, input, f0, ef, nf) → eeval(ef, Cons(nf, Nil), Cons(input, Nil), p)
eeval[Let][Let][Let](e, ns, vs, p, ef, nf, v) → eeval(ef, Cons(nf, Nil), Cons(v, Nil), p)
Types:
eeval :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
Fun :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[False][Let] :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
lookbody :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
Eq :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[True][Ite] :: False:True → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eqExp :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → False:True
Error :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[False][Ite] :: False:True → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
False :: False:True
F :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
T :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
ITE' :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[Ite] :: False:True → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
checkConstrExp :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → False:True
Bsf :: getBsfOp → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[Let] :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
Var :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
lookvar :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
run :: Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
Cons :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil
run[Let][Let] :: Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
and :: False:True → False:True → False:True
True :: False:True
!EQ :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → False:True
lookname :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
lookname[Ite] :: False:True → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
lookbody[Ite] :: False:True → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getVar :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getIfTrue :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getIfGuard :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getIfFalse :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getFuncName :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getFuncExp :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getEqSecond :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getEqFirst :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getConst :: Cst → getConst
Cst :: getConst → Cst
getBsfSecondTerm :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
getBsfOp :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → getBsfOp
getBsfFirstTerm :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
apply :: getBsfOp → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
apply[Ite] :: False:True → getBsfOp → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
lookvar[Ite] :: False:True → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eqOps :: a → b → False:True
S :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
0' :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[False][Let][Let] :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[Let][Let][Let] :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
eeval[Let][Let] :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Cons:Nil → Cons:Nil → Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
run[Let] :: Cons:Nil → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0' → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
Nil :: Cons:Nil
hole_Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'1_3 :: Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
hole_Cons:Nil2_3 :: Cons:Nil
hole_False:True3_3 :: False:True
hole_getBsfOp4_3 :: getBsfOp
hole_getConst5_3 :: getConst
hole_Cst6_3 :: Cst
hole_a7_3 :: a
hole_b8_3 :: b
gen_Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'9_3 :: Nat → Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'
gen_Cons:Nil10_3 :: Nat → Cons:Nil
Generator Equations:
gen_Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'9_3(0) ⇔ F
gen_Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'9_3(+(x, 1)) ⇔ Fun(F, gen_Fun:Eq:Error:F:T:ITE':Bsf:Var:S:0'9_3(x))
gen_Cons:Nil10_3(0) ⇔ Nil
gen_Cons:Nil10_3(+(x, 1)) ⇔ Cons(F, gen_Cons:Nil10_3(x))
The following defined symbols remain to be analysed:
eqExp, eeval, eeval[False][Let], lookvar, lookname
They will be analysed ascendingly in the following order:
eeval = eeval[False][Let]
eqExp < eeval
lookvar < eeval
lookname < eeval[False][Let]